l1, l2:IdLnk, d1, d2:tg:Id fp Type.
(l1 = l2  d1 || d2)  lnk-decl(l1;d1) || lnk-decl(l2;d2) 

latex

Definitions	IdLnk, IdDeq, Id, Dec(P), P  Q, SQType(T), {T}, f || g, f(x), P & Q, Prop, b, x  dom(f), KindDeq, a:A fp B(a), Top, x. t(x), lnk-decl(l;dt), x:A. B(x), P  Q, t  T, Knd, map(f;as), P  Q, rcv(l,tg), x:A. B(x), P  Q, deq-member(eq;x;L), (x  l), A, False
Lemmas	rcv one one, l member wf, deq-member wf, and functionality wrt iff, Knd sq, rcv wf, member map, map wf, assert-deq-member, Knd wf, lnk-decl wf, fpf-trivial-subtype-top, Kind-deq wf, fpf-dom wf, assert wf, IdLnk sq, IdLnk wf, decidable equal IdLnk, Id wf, fpf wf, id-deq wf, fpf-compatible wf